#include "symbolics.h"
#include <iostream>
#include <fstream>
#include <cstdlib>//abort

namespace divine {

//---------Node----------
Node::Node(): arity( 0 ) {}

Node::Node( int n ): arity( n ) {
  heirs.resize( n );
}

Node::Node( const Node &n ) {
  type = n.type;
  op = n.op;
  arity = n.arity;
  name = n.name;
  round = n.round;
  value = n.value;
  heirs = n.heirs;
}

int Node::size() {
  int retVal = 0;
  retVal += sizeof( TYPE );
  retVal += sizeof( OPTYPE );
  retVal += 16;
  retVal += 4 * heirs.size();
  return retVal;
}

void Node::rebuild( char **tab ) {
  blobRead< TYPE >( &type, tab );
  blobRead< OPTYPE >( &op, tab );
  blobRead< int >( &arity, tab );
  blobRead< int >( &name, tab );
  blobRead< int >( &round, tab );
  blobRead< uint32_t >( &value, tab );
  heirs.resize( arity );
  for ( int i = 0; i < arity; i++ ) {
    blobRead< uint32_t >( &(heirs.at( i )), tab );
  }
}

void Node::store( char **tab ) {
  blobWrite< TYPE >( tab, &type );
  blobWrite< OPTYPE >( tab, &op );
  blobWrite< int >( tab, &arity );
  blobWrite< int >( tab, &name );
  blobWrite< int >( tab, &round );
  blobWrite< uint32_t >( tab, &value );
  for ( int i = 0; i < arity; i++ ) {
    blobWrite< uint32_t >( tab, &(heirs.at( i )) );
  }
}
//---------Node-----------
 
//----------Expr----------
Expr::Expr( SMTRep *_smt ): smt( _smt ) {}

Expr::Expr( Expr &e ) {
  nodes = e.nodes;
  smt = e.smt;
}

Expr::Expr( const Expr &e ) {
  nodes = e.nodes;
  smt = e.smt;
}

Expr::Expr( Expr *e ) {
  nodes = e->nodes;
  smt = e->smt;
}

void Expr::round( int r ) {
  for ( int i = 0; i < nodes.size(); i++ )
    if ( nodes.at( i ).type == INVAR )
      nodes.at( i ).round = r;
}

void Expr::subs( int order, Expr *e ) {
  std::vector< int > holders;
  //first find out if there are any such named variables
  //and remember their positions
  for ( int i = 0; i < nodes.size(); i++ ) {
    if ( nodes.at( i ).type == VAR && nodes.at( i ).name == order )
      holders.push_back( i );
  }
    
  if ( holders.empty() )
    return;

  //update a copy of the expression "e", so that the individual nodes
  //point to resulting positions (increase by size of this expression)
  std::vector< Node > tempVe = e->nodes;
  for ( int j = 0; j < tempVe.size(); j++ )
    for ( int i = 0; i < tempVe.at( j ).heirs.size(); i++ )
      tempVe.at( j ).heirs.at( i ) += nodes.size() - 1;

  //copy over each node, bar the root
  if ( tempVe.size() == 0 )
    abort();
  for ( int i = 1; i != tempVe.size(); i++ )
    nodes.push_back( tempVe.at( i ) );

  //replace the root (of e) for every stored position
  for ( int i = 0; i < holders.size(); i++ ) {
    nodes.at( holders.at( i ) ) = tempVe.at( 0 );
  }
}

std::string Expr::translate( int i, bool B ) {
  if ( nodes.size() == 0 )
    return "";
  return tran( 0, B, i );
}

std::string Expr::print() {
  std::stringstream s;
  for ( int i = 0; i < nodes.size(); i++ ) {
    s << i << "|" << nodes.at( i ).type  << ": ";
    for ( int j = 0; j < nodes.at( i ).heirs.size(); j++ ) {
      s << nodes.at( i ).heirs.at( j ) << " ";
    }
    s << std::endl;
  }
  return s.str();
}

std::string Expr::convert( uint32_t val, bool Bool ) {
  std::stringstream str;
  if ( Bool )
    return (val ? "true" : "false");
  str << "#b";
  for ( uint32_t i = 0; i < bit_width; i++ )
    str << ((val >> ((bit_width-i)-1))&1) ? "1" : "0";
  return str.str();
}

std::string Expr::convert( std::string val, bool Bool ) {
  if ( !Bool )
    return val;
  std::stringstream str;
  str << "(= " << val << " #b";
  for ( uint32_t i = 0; i < bit_width; i++ )
    str << "0";
  str << ")";
  return str.str();
}

//translate one node, Bool if we expect it to be Bolean
//k is a helper to distinguish left and right copies of inports
std::string Expr::tran( uint32_t i, bool Bool, int k ) {
  Node tempN = nodes.at( i );
  if ( tempN.arity == 0 ) {
    std::stringstream s, str;
    switch ( tempN.type ) {
    case CON :
      s << " " << convert( tempN.value, Bool );
      break;
    case INVAR :
      if ( k ) {
        if ( k == 3 )
          str << "y" << tempN.round * smt->os.inports_range.size() + tempN.name;
        else
          str << smt->os.inports_name.at( tempN.name ) << tempN.round << k;
      }
      else
        str << smt->os.inports_name.at( tempN.name ) << tempN.round;
      convert( str.str(), Bool );
      s << " " << convert( str.str(), Bool );
      break;
    case VAR :
      str << smt->os.delays_name.at( tempN.name );
      s << " " << convert( str.str(), Bool );
      break;
    }
    return s.str();
  }
  
  std::string first, second, third;
  if ( tempN.arity > 0 ) first = tran( tempN.heirs.at( 0 ), false, k );
  if ( tempN.arity > 1 ) second = tran( tempN.heirs.at( 1 ), false, k );
  if ( tempN.arity > 2 ) third = tran( tempN.heirs.at( 2 ), false, k );

  std::stringstream temp;
  switch ( tempN.op ) {
  case MIN : //so far only two
    return "(ite (bvult" + first + second + ") " + first + " " + second
      + ")";
  case MAX : //so far only two
    return "(ite (bvugt" + first + second + ") " + first + " " + second
      + ")";
  case SWITCH :
    first = tran( tempN.heirs.at( 0 ), Bool, k );
    second = tran( tempN.heirs.at( 1 ), true, k );
    third = tran( tempN.heirs.at( 2 ), Bool, k );
    return "(ite " + second + " " + first + " " + third + ")";
  case LT :
    return "(bvult" + first + second + ")";
  case LE :
    return "(bvule" + first + second + ")";
  case GT :
    return "(bvugt" + first + second + ")";
  case GE :
    return "(bvuge" + first + second + ")";
  case NEQ :
    first = tran( tempN.heirs.at( 0 ), Bool, k );
    second = tran( tempN.heirs.at( 1 ), Bool, k );
    return "(distinct" + first + second + ")";
  case EQ :
    first = tran( tempN.heirs.at( 0 ), Bool, k );
    second = tran( tempN.heirs.at( 1 ), Bool, k );
    return "(=" + first + second + ")";
  case NOT :
    first = tran( tempN.heirs.at( 0 ), true, k );
    return "(not" + first + ")";
  case AND :
    first = tran( tempN.heirs.at( 0 ), true, k );
    second = tran( tempN.heirs.at( 1 ), true, k );
    return "(and" + first + second + ")";
  case OR :
    first = tran( tempN.heirs.at( 0 ), true, k );
    second = tran( tempN.heirs.at( 1 ), true, k );
    return "(or" + first + second + ")";
  case IMP :
    first = tran( tempN.heirs.at( 0 ), true, k );
    second = tran( tempN.heirs.at( 1 ), true, k );
    return "(=>" + first + second + ")";
  case XOR :
    return "(bvxnor" + first + second + ")"; //???
  case NAND :
    return "(bvnand" + first + second + ")";
  case NOR :
    return "(bvnor" + first + second + ")";
  case PLUS :
    if ( Bool ) {
    temp << "(distinct (bvadd" + first + second + ") #b";
      for ( uint32_t i = 0; i < bit_width; i++ )
        temp << "0";
      temp << ")";
      return temp.str();
    }
    return "(bvadd" + first + second + ")";
  case TIMES :
    if ( Bool ) {
    temp << "(distinct (bvmul" + first + second + ") #b";
      for ( uint32_t i = 0; i < bit_width; i++ )
        temp << "0";
      temp << ")";
      return temp.str();
    }
    return "(bvmul" + first + second + ")";
  case CAST : //ignore it for now (vars are 32bit by default)
    first = tran( tempN.heirs.at( 0 ), true, k );
    if ( Bool )
      return first;
    return "(ite " + first + " " + convert( 1, false ) + " "
      + convert( 0, false ) + ")";
  default :
    std::cerr << "Error: Unknown literal." << std::endl;
    abort();
  }
}

void Expr::clear() {
  root = 0;
  nodes.clear();
}

int Expr::size() {
  int retVal = 0;
  retVal += 4;
  for ( int i = 0; i < nodes.size(); i++ )
    retVal += nodes.at( i ).size();
  return retVal;
}

void Expr::rebuild( char **tab ) {
  int nodes_size;
  blobRead< int >( &nodes_size, tab );
  nodes.resize( nodes_size );
  for ( int i = 0; i < nodes.size(); i++ )
    nodes.at( i ).rebuild( tab );
}

void Expr::store( char **tab ) {
  int nodes_size = nodes.size();
  blobWrite< int >( tab, &nodes_size );
  for ( int i = 0; i < nodes.size(); i++ )
    nodes.at( i ).store( tab );
}
//----------Expr----------

//--------SMTRep-------------
  SMTRep::SMTRep(): round( 0 ) { counter = 0; times.resize( 16 ); cond_tick = false; }

SMTRep::SMTRep( SMTRep *r ) {
  os = r->os;
  offset = r->offset;
  counter = r->counter;
  times = r->times;
}

void SMTRep::tick() {
  if ( cond_tick )
    return;
  cond_tick = true;
  std::vector< Expr > newDelays;
  Expr tempE( this );
  round++;
  if ( round > 15 ) {//debug
    for ( int i = 0; i < times.size(); i++ ) {
      std::cout << i << " " << times.at( i ).checks << " "
                << times.at( i ).time << " "
                << times.at( i ).size << " "
                << times.at( i ).state_size << " "
                << times.at( i ).assertions << std::endl;
    }
    abort();//debug
  }
  //times.push_back( std::make_pair( 0, 0 ) );//debug
  for ( int i = 0; i < os.delays_expr.size(); i++ ) {
    tempE = os.delays_expr.at( i );
    tempE.round( round );
    for ( int i = 0; i < curDelays.size(); i++ ) {
      tempE.subs( i, &(curDelays.at( i )) );
    }
    newDelays.push_back( tempE );
  }
  curDelays = newDelays;
}

int SMTRep::size() {
  int retVal = (20 - offset);
  retVal += 2*sizeof(int); //round+in_val_size
  retVal += in_values.size() * sizeof(uint32_t);
  for ( int i = 0; i < curDelays.size(); i++ ) 
    retVal += curDelays.at( i ).size();
  retVal += sizeof(int); //pc_size
  for ( int i = 0; i < pc.size(); i++ )
    retVal += pc.at( i ).size();
  return retVal;
}

void SMTRep::read( char *tab ) {
  char *table = tab;
  table += (20 - offset);
  blobRead< int >( &(round), &(table) );
  int in_values_size;
  blobRead< int >( &(in_values_size), &(table) );
  in_values.resize( in_values_size );
  for ( int i = 0; i < in_values_size; i++ ) {
    blobRead< uint32_t >( &(in_values.at( i )), &(table) );
  }
  curDelays.resize( os.delays_expr.size() );
  for ( int i = 0; i < curDelays.size(); i++ ) {
    curDelays.at( i ).smt = this;
    curDelays.at( i ).rebuild( &(table) );
  }
  int pc_size;
  blobRead< int >( &(pc_size), &(table) );
  pc.resize( pc_size );
  for ( int i = 0; i < pc_size; i++ ) {
    pc.at( i ).smt = this;
    pc.at( i ).rebuild( &(table) );
  }
}

void SMTRep::write( char *tab ) {
  char *table = tab;
  table += ((20 - offset) - sizeof(SMTRep*));
  SMTRep *r = this;
  blobWrite< SMTRep* >( &(table), &(r) );
  blobWrite< int >( &(table), &(round) );
  int in_values_size = in_values.size();
  blobWrite< int >( &(table), &(in_values_size) );
  for ( int i = 0; i < in_values_size; i++ ) {
    blobWrite< uint32_t >( &(table), &(in_values.at( i )) );
  }
  for ( int i = 0; i< curDelays.size(); i++ ) {
    curDelays.at( i ).store( &(table) );
  }
  int pc_size = pc.size();
  blobWrite< int >( &(table), &(pc_size) );
  for ( int i = 0; i < pc_size; i++ ) {
    pc.at( i).store( &(table) );
  }
}

//just for testing, some sanity checks
void SMTRep::verify_consistency() {
  for ( int i = 0; i < os.delays_expr.size(); i++ )
    if ( this != os.delays_expr.at( i ).smt )
      abort();
  for ( int i = 0; i < os.outports_expr.size(); i++ )
    if ( this != os.outports_expr.at( i ).smt )
      abort();
  for ( int i = 0; i < curDelays.size(); i++ ) {
    if ( this != curDelays.at( i ).smt )
      abort();
  }
}

void SMTRep::initialise() {
  Expr e( this );
  Node n( 0 );
  n.type = CON;
  n.value = 0;
  e.nodes.push_back( n );
  for ( int i = 0; i < os.delays_expr.size(); i++ ) {
    curDelays.push_back( e );
  }
}

std::string SMTRep::print() {
  std::stringstream s;
  s << "---------------------------" << std::endl;
  s << "[";
  for ( int i = 0; i < in_values.size(); i++ )
    s << in_values.at( i ) << " ";
  s << "]" << std::endl;
  s << "-----------" << std::endl;
  s << "{";
  for ( int i = 0; i < curDelays.size(); i++ )
    s << curDelays.at( i ).translate( 0, false ) << " ";
  s << "}" << std::endl;
  s << "-----------" << std::endl;
  s << "<";
  for ( int i = 0; i < pc.size(); i++ )
    s << pc.at( i ).translate( 0, false ) << " ";
  s << ">" << std::endl;
  s << "---------------------------";
  return s.str();
}

std::string SMTRep::convert( uint32_t val, bool Bool ) {
  std::stringstream str;
  if ( Bool )
    return (val ? "true" : "false");
  str << "#b";
  for ( uint32_t i = 0; i < bit_width; i++ )
    str << ((val >> ((bit_width-i)-1))&1) ? "1" : "0";
  return str.str();
}

int SMTRep::by_name( std::string n ) {
  for ( int i = 0; i < os.delays_name.size(); i++ )
    if ( os.delays_name.at( i ) == n )
      return i;
  for ( int i = 0; i < os.outports_name.size(); i++ )
    if ( os.outports_name.at( i ) == n )
      return i;
  for ( int i = 0; i < os.inports_name.size(); i++ )
    if ( os.inports_name.at( i ) == n )
      return i;
  abort();
  //shouldn't get here
}

//check satisfiability of the current path condition
bool SMTRep::pc_sat( bool last ) {
  //std::cout << "tick " << round << std::endl;//debug
  //std::cout << "number: " << ++counter << std::endl;//debug
  //std::cout << round << std::endl;//debug
  times.at( round ).checks++;
  startTimer();
  pc.insert( pc.end(), lastPC.begin(), lastPC.end() );
  std::ofstream smt_input;
  smt_input.open("in.smt2");
  smt_input << "(set-option :produce-models true)\n";
  smt_input << "(set-logic QF_BV)\n";
  //declare inport variables
  for ( int i = 0; i < round + 1; i++ ) {
    for ( int j = 0; j < os.inports_range.size(); j++ )
      smt_input << "(declare-fun " << os.inports_name.at( j ) << i
                << " () (_ BitVec " << bit_width << "))\n";
  }
  //declare helper variables for inport differentiation
  if ( distinct_inports != 0 ) {
    for ( int i = 0; i < os.inports_range.size(); i++ ) {
      for ( int j = 0; j < distinct_inports; j++ ) {
        smt_input << "(declare-fun " << os.inports_name.at( i ) << "x"
                  << j << " () (_ BitVec " << bit_width << "))\n";
      }
    }
  }
  //write down boundaries
  for ( int i = 0; i < round + 1; i++ ) {
    for ( int j = 0; j < os.inports_range.size(); j++ ) {
      smt_input << "(assert (bvuge " << os.inports_name.at( j ) << i
                << " " << convert( os.inports_range.at( j ).first, false )
                << "))\n";
      smt_input << "(assert (bvule " << os.inports_name.at( j ) << i
                << " " << convert( os.inports_range.at( j ).second, false )
                << "))\n";
    }
  }
  //first heuristic: allow only k different values for inports
  if ( distinct_inports != 0 ) {
    for ( int i = 0; i < os.inports_range.size(); i++ ) {
      smt_input << "(assert (distinct ";
      for ( int j = 0; j < distinct_inports; j++ ) {
        smt_input << os.inports_name.at( i ) << "x" << j << " ";
      }
      smt_input << "))\n";
    }
    for ( int i = 0; i < round + 1; i++ ) {
      for ( int j = 0; j < os.inports_range.size(); j++ ) {
        smt_input << "(assert (or ";
        for ( int k = 0; k < distinct_inports; k++ ) {
          smt_input << "(= " << os.inports_name.at( j ) << i << " "
                    << os.inports_name.at( j ) << "x" << k << ")";
        }
        smt_input << "))\n";
      }
    }
  }
  //write down the assertion making up the pc
  for ( int i = 0; i < pc.size(); i++ ) {
    smt_input << "(assert " + pc.at( i ).translate( 0, true ) + ")\n";
  }
  smt_input << "(check-sat)\n";
  //we need the last round for counterexample
  smt_input << "(get-value (";
  for ( int i = 0; i < os.inports_range.size(); i++ ) {
    smt_input << os.inports_name.at( i ) << round << " ";
  }
  smt_input << "))\n";
  smt_input.close();
  //debug
  //FILE *f = fopen( "/home/xbauch/divines/z3_divine/_build/tools/in.smt2", "r" );
  std::ifstream file( "in.smt2", std::ios::binary | std::ios::ate );
  times.at( round ).size += file.tellg();
  file.close();
  times.at( round ).assertions += pc.size();
  //debug
  //call the smt solver
  system( "/home/xbauch/z3/build/z3 -smt2 /home/xbauch/divines/z3_divine/_build/tools/in.smt2 > /home/xbauch/divines/z3_divine/_build/tools/out.txt" );
  //read the result and if sat, then store the counterexample inports
  std::ifstream smt_output;
  smt_output.open( "out.txt", std::ifstream::in );
  int ch = smt_output.get();
  bool retVal;
  if ( ch == '(' ) {
    std::cerr << "Error: wrong input for SMT." << std::endl;
    abort();
  }
  if ( ch == 'u' ) {
    retVal = false;
  }
  else {
    char line[ 256 ];
    smt_output.getline( line, 256 );
    //read the lines, parse the hexa values of the generated model
    for ( int i = 0; i < os.inports_range.size(); i++ ) {
      smt_output.getline( line, 256 );
      for ( int j = 0; j < 256; j++ ) {
        if ( line[ j ] == '#' ) {
          line[ j ] = '0';
          std::string tempString( line + j, line + j + 4 );
          std::stringstream tempStream;
          tempStream << std::hex << tempString;
          uint32_t tempValue;
          tempStream >> tempValue;
          in_values.push_back( tempValue );
          break;
        }
      }
    }
    retVal = true;
  }
  bool erase = true;
  if ( last ) {
    lastPC.clear();
    if ( retVal ) {
      cond_tick = false;
      erase = false;
      times.at( round ).state_size += size();
    }
  }
  if ( erase )
    pc.erase( pc.end() - lastPC.size(), pc.end() );
  // else
  //   round--;
  //std::cout << "time: " << endTimer() << std::endl;//debug
  times.at( round ).time += endTimer();
  return retVal;
}

//called from the buchi automaton
//add one more assertion to the current path condition
void SMTRep::addToPath( Expr *e ) {
  Expr tempE = *e;
  tempE.round( round );
  std::vector< Expr > tempV;
  //substitute current delays in outports
  for ( int i = 0; i < os.outports_expr.size(); i++ ) {
    Expr tempEE = os.outports_expr.at( i );
    for ( int i = 0; i < curDelays.size(); i++ ) {
      tempEE.subs( i, &(curDelays.at( i )) );
    }
    tempV.push_back( tempEE );
  }
  //substitute delays in the expression
  for ( int i = 0; i < curDelays.size(); i++ ) {
    tempE.subs( i, &(curDelays.at( i )) );
  }
  int n = curDelays.size();
  //substitute outports in the expression
  for ( int i = 0; i < tempV.size(); i++ ) {
    tempE.subs( i + n, &(tempV.at( i )) );
  }

  lastPC.push_back( tempE );
}

void SMTRep::translate( std::vector< Expr > *v, char *blob ) {
  SMTRep rep( this );
  rep.read( blob + offset );
  *v = rep.curDelays;
}

int SMTRep::get_round( std::vector< Expr > *vec ) {
  int max = 0;
  for ( int i = 0; i < vec->size(); i++ ) {
    for ( int j = 0; j < vec->at( i ).nodes.size(); j++ ) {
      if ( vec->at( i ).nodes.at( j ).type == INVAR &&
           vec->at( i ).nodes.at( j ).round > max )
        max = vec->at( i ).nodes.at( j ).round;
    }
  }
  return max;
}

bool SMTRep::check_ide( std::vector< Expr > *del1, std::vector< Expr > *pc1,
                        std::vector< Expr > *del2, std::vector< Expr > *pc2 ) {
  return false;//debug
  std::ofstream smt_input;
  smt_input.open("in.smt2");
  smt_input << "(set-option :mbqi true)\n";
  smt_input << "(define-sort Full () (_ BitVec " << bit_width << "))\n";
  //declare the variables
  for ( int i = 0; i < os.delays_expr.size(); i++ ) {
    smt_input << "(declare-fun " + os.delays_name.at( i )
      + "1 () (_ BitVec " << bit_width << "))\n";
    smt_input << "(declare-fun " + os.delays_name.at( i )
      + "2 () (_ BitVec " << bit_width << "))\n";
  }
  //declare inports, also decorated for each delay
  int max_round_1 = get_round( del1 );
  int max_round_2 = get_round( del2 );
  for ( int i = 0; i < max_round_1 + 1; i++ ) {
    for ( int j = 0; j < os.inports_range.size(); j++ )
      smt_input << "(declare-fun " << os.inports_name.at( j ) << i << "1"
                << " () (_ BitVec " << bit_width << "))\n";
  }
  for ( int i = 0; i < max_round_2 + 1; i++ ) {
    for ( int j = 0; j < os.inports_range.size(); j++ )
      smt_input << "(declare-fun " << os.inports_name.at( j ) << i << "2"
                << " () (_ BitVec " << bit_width << "))\n";
  }
  //declare helper variables for inport differentiation
  //also their copies for quantified versions
  if ( distinct_inports != 0 ) {
    for ( int i = 0; i < os.inports_range.size(); i++ ) {
      for ( int j = 0; j < distinct_inports; j++ ) {
        smt_input << "(declare-fun " << os.inports_name.at( i ) << "x1"
                  << j << " () (_ BitVec " << bit_width << "))\n";
        smt_input << "(declare-fun " << os.inports_name.at( i ) << "x2"
                  << j << " () (_ BitVec " << bit_width << "))\n";
        smt_input << "(declare-fun " << os.inports_name.at( i ) << "xy1"
                  << j << " () (_ BitVec " << bit_width << "))\n";
        smt_input << "(declare-fun " << os.inports_name.at( i ) << "xy2"
                  << j << " () (_ BitVec " << bit_width << "))\n";
      }
    }
  }
  //write down boundaries
  for ( int i = 0; i < max_round_1 + 1; i++ ) {
    for ( int j = 0; j < os.inports_range.size(); j++ ) {
      smt_input << "(assert (bvuge " << os.inports_name.at( j ) << i << "1"
                << " " << convert( os.inports_range.at( j ).first, false )
                << "))\n";
      smt_input << "(assert (bvule " << os.inports_name.at( j ) << i << "1"
                << " " << convert( os.inports_range.at( j ).second, false )
                << "))\n";
    }
  }
  for ( int i = 0; i < max_round_2 + 1; i++ ) {
    for ( int j = 0; j < os.inports_range.size(); j++ ) {
      smt_input << "(assert (bvuge " << os.inports_name.at( j ) << i << "2"
                << " " << convert( os.inports_range.at( j ).first, false )
                << "))\n";
      smt_input << "(assert (bvule " << os.inports_name.at( j ) << i << "2"
                << " " << convert( os.inports_range.at( j ).second, false )
                << "))\n";
    }
  }
  //first heuristic: allow only k different values for inports
  if ( distinct_inports != 0 ) {
    for ( int i = 0; i < os.inports_range.size(); i++ ) {
      smt_input << "(assert (distinct ";
      for ( int j = 0; j < distinct_inports; j++ ) {
        smt_input << os.inports_name.at( i ) << "x1" << j << " ";
      }
      smt_input << "))\n";
    }
    for ( int i = 0; i < os.inports_range.size(); i++ ) {
      smt_input << "(assert (distinct ";
      for ( int j = 0; j < distinct_inports; j++ ) {
        smt_input << os.inports_name.at( i ) << "x2" << j << " ";
      }
      smt_input << "))\n";
    }
    //and now for the copies for quantified versions
    for ( int i = 0; i < os.inports_range.size(); i++ ) {
      smt_input << "(assert (distinct ";
      for ( int j = 0; j < distinct_inports; j++ ) {
        smt_input << os.inports_name.at( i ) << "xy1" << j << " ";
      }
      smt_input << "))\n";
    }
    for ( int i = 0; i < os.inports_range.size(); i++ ) {
      smt_input << "(assert (distinct ";
      for ( int j = 0; j < distinct_inports; j++ ) {
        smt_input << os.inports_name.at( i ) << "xy2" << j << " ";
      }
      smt_input << "))\n";
    }
    for ( int i = 0; i < max_round_1 + 1; i++ ) {
      for ( int j = 0; j < os.inports_range.size(); j++ ) {
        smt_input << "(assert (or ";
        for ( int k = 0; k < distinct_inports; k++ ) {
          smt_input << "(= " << os.inports_name.at( j ) << i << "1 "
                    << os.inports_name.at( j ) << "x1" << k << ")";
        }
        smt_input << "))\n";
      }
    }
    for ( int i = 0; i < max_round_2 + 1; i++ ) {
      for ( int j = 0; j < os.inports_range.size(); j++ ) {
        smt_input << "(assert (or ";
        for ( int k = 0; k < distinct_inports; k++ ) {
          smt_input << "(= " << os.inports_name.at( j ) << i << "2 "
                    << os.inports_name.at( j ) << "x2" << k << ")";
        }
        smt_input << "))\n";
      }
    }
  }
  //write down the assertion making up the pcs
  for ( int i = 0; i < pc1->size(); i++ ) {
    smt_input << "(assert " + pc1->at( i ).translate( 1, true ) + ")\n";
  }
  for ( int i = 0; i < pc2->size(); i++ ) {
    smt_input << "(assert " + pc2->at( i ).translate( 2, true ) + ")\n";
  }
  //fu
  std::string first, second;
  for ( int i = 0; i < os.delays_expr.size(); i++ ) {
    first = os.delays_name.at( i ) + "1";
    second = os.delays_name.at( i ) + "2";
    smt_input << "(assert (= " + first + " " + del1->at( i ).translate( 1, false )
      + "))\n";
    smt_input << "(assert (= " + second + " " + del2->at( i ).translate( 2, false )
      + "))\n";
  }
  smt_input << "(assert (or ";
  for ( int i = 0; i < os.delays_expr.size(); i++ ) {
    first = os.delays_name.at( i ) + "1";
    second = os.delays_name.at( i ) + "2";
    smt_input << "(forall (";
    for ( int j = 0; j < max_round_2 + 1; j++ ) {
      for ( int k = 0; k < os.inports_range.size(); k++ ) {
        smt_input << "(y" << j * os.inports_range.size() + k << " Full)";
      }
    }
    smt_input << ") (=> (and ";
    for ( int j = 0; j < max_round_2 + 1; j++ ) {
      for ( int k = 0; k < os.inports_range.size(); k++ ) {
        smt_input << "(bvuge y" << j * os.inports_range.size() + k
                  << " " << convert( os.inports_range.at( j ).first, false )
                  << ") ";
        smt_input << "(bvule y" << j * os.inports_range.size() + k
                  << " " << convert( os.inports_range.at( j ).second, false )
                  << ") ";
      }
    }
    //associate y's with the differentiated inports
    if ( distinct_inports != 0 ) {
      for ( int j = 0; j < max_round_2 + 1; j++ ) {
        for ( int k = 0; k < os.inports_range.size(); k++ ) {
          smt_input << "(or ";
          for ( int l = 0; l < distinct_inports; l++ ) {
            smt_input << "(= y" << j * os.inports_range.size() + k << " "
                      << os.inports_name.at( k ) << "xy2" << l << ")";
          }
          smt_input << ") ";
        }
      }
    }                            
    for ( int j = 0; j < pc2->size(); j++ ) {
      smt_input << pc2->at( j ).translate( 3, true );
    }
    smt_input << ")(distinct " << first << " "
              << del2->at( i ).translate( 3, false ) << "))) ";
    smt_input << "(forall (";
    for ( int j = 0; j < max_round_1 + 1; j++ ) {
      for ( int k = 0; k < os.inports_range.size(); k++ ) {
        smt_input << "(y" << j * os.inports_range.size() + k << " Full)";
      }
    }
    smt_input << ") (=> (and ";
    for ( int j = 0; j < max_round_1 + 1; j++ ) {
      for ( int k = 0; k < os.inports_range.size(); k++ ) {
        smt_input << "(bvuge y" << j * os.inports_range.size() + k
                  << " " << convert( os.inports_range.at( j ).first, false )
                  << ") ";
        smt_input << "(bvule y" << j * os.inports_range.size() + k
                  << " " << convert( os.inports_range.at( j ).second, false )
                  << ") ";
      }
    }
    //associate y's with the differentiated inports
    if ( distinct_inports != 0 ) {
      for ( int j = 0; j < max_round_1 + 1; j++ ) {
        for ( int k = 0; k < os.inports_range.size(); k++ ) {
          smt_input << "(or ";
          for ( int l = 0; l < distinct_inports; l++ ) {
            smt_input << "(= y" << j * os.inports_range.size() + k << " "
                      << os.inports_name.at( k ) << "xy1" << l << ")";
          }
          smt_input << ") ";
        }
      }
    }                            
    for ( int j = 0; j < pc1->size(); j++ ) {
      smt_input << pc1->at( j ).translate( 3, true );
    }
    smt_input << ")(distinct " << second << " "
              << del1->at( i ).translate( 3, false ) << "))) ";
  }
  smt_input << "))\n";
  smt_input << "(check-sat)\n";
  smt_input.close();
  abort();
  system( "/home/xbauch/z3/build/z3 -smt2 /home/xbauch/divines/z3_divine/_build/tools/in.smt2 > /home/xbauch/divines/z3_divine/_build/tools/out.txt" );
  //read the result
  std::ifstream smt_output;
  smt_output.open( "out.txt", std::ifstream::in );
  int ch = smt_output.get();
  if ( ch == '(' ) {
    std::cerr << "wrong input for smt." << std::endl;
    abort();
  }
  std::cout << "success" << std::endl;//debug
  abort();//debug
  if ( ch == 'u' ) {
    return true;
  }
  else {
    return false;
  }
}

int SMTRep::find( std::vector< std::vector< Expr > > *delays,
                  std::vector< std::vector< Expr > > *pcs, char *blob ) {
  read( blob + offset );
  for ( int i = 0; i < delays->size(); i++ )
    if ( check_ide( &(delays->at( i )), &(pcs->at( i )),
                    &(curDelays), &(pc) ) )
      return i;
  return delays->size();
}

int SMTRep::addIfNew( std::vector< std::vector< Expr > > *delays,
                      std::vector< std::vector< Expr > > *pcs, char *blob ) {
  read( blob + offset );
  for ( int i = 0; i < delays->size(); i++ )
    if ( check_ide( &(delays->at( i )), &(pcs->at( i )),
                    &(curDelays), &(pc) ) )
      return i;
  delays->push_back( curDelays );
  pcs->push_back( pc );
  return -1;
}

void SMTRep::add( std::vector< std::vector< Expr > > *delays,
                  std::vector< std::vector< Expr > > *pcs, char *blob ) {
  read( blob + offset );
  delays->push_back( curDelays );
  pcs->push_back( pc );
}

}
